FDL - Nuprl Definition : int_ring

Nuprl Definition : int_ring

-rng
== <

== ,

u,v. (u =

v)
== ,

u,v. u

z v
== ,

u,v. u+v
== , 0
== ,

u.-u
== ,

u,v. u * v
== , 1
== ,

u,v. if (v =

0) then inr

else inl (u

v) fi >

Up rings 1

Wellformedness Lemmas int ring wf

Definitions , i z j, n+m, -n, n * m, <a, b>, x.A(x), if b then t else f fi , (i = j), #$n, inr x , , inl x , n m